T:Type, eq:EqDecider(T), f:(TT).
retraction(T;f)  (x:T. f(f**(x)) = f**(x) & f**(x) is f*(x)) 

latex

Definitions

x:A  B(x), x:AB(x), strong-subtype(A;B), Type, EqDecider(T), left + right, P  Q, False, A, A  B, , {x:A| B(x)} , x:A. B(x), retraction(T;f), t  T, i  j , Outcome, -n, n - m, Void, #$n, f(a), n+m, f**(x), y is f*(x), s = t, P & Q, a < b, P  Q, x:A. B(x), , , b, eqof(d), P  Q, P  Q, , p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, , x f y, =, a < b, =, =, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), b, p  q, p  q, p q, ff, tt, Unit, |g|, S  T, y=f*(x) via L, type List, A List, [], [car / cdr], {i..j}, l[i], hd(l), tl(l), {T}, SQType(T), s ~ t, i  j < k, Dec(P), Atom, x,y:A//B(x;y), b | a, a ~ b, |p|, a  b, a <p b, a < b, A c B, |r|, xL. P(x), (xL.P(x)), , Atom$n, , r  s, r < s, q-rel(r;x), <a, b>, t  ...$L, ||as||, last(L)

Lemmas

int seg wf, false wf, select wf, length nil, length cons, non neg length, length wf1, le wf, decidable int equal, guard wf, fun-path wf, fun-connected transitivity, fun-connected weakening eq, eqtt to assert, not wf, bool wf, iff transitivity, eqff to assert, assert of bnot, not functionality wrt iff, iff wf, rev implies wf, deq property, assert wf, ge wf, nat properties, deq wf, retraction wf, nat wf, nat ind tp, fun-connected wf